Applications of Polyhedral Computations to the Analysis and Verification of Hardware and Software Systems

摘要

Convex polyhedra are the basis for several abstractions used in staticanalysis and computer-aided verification of complex and sometimes missioncritical systems. For such applications, the identification of an appropriatecomplexity-precision trade-off is a particularly acute problem, so that theavailability of a wide spectrum of alternative solutions is mandatory. Wesurvey the range of applications of polyhedral computations in this area; givean overview of the different classes of polyhedra that may be adopted; outlinethe main polyhedral operations required by automatic analyzers and verifiers;and look at some possible combinations of polyhedra with other numericalabstractions that have the potential to improve the precision of the analysis.Areas where further theoretical investigations can result in importantcontributions are highlighted.